T:Type, f:(TT), x, y:T, L:(T List). x=f*(y) via L   

latex

Definitions	s = t, t  T, False, Type, x:AB(x), type List, a < b, , P  Q, A, i  j , ||as||, b, hd(l), True, x:A. B(x), <a, b>, #$n, , last(L), n+m, l[i], f(a), x:A  B(x), P & Q, n - m, {i..j}, Void, A c B, y=f*(x) via L
Lemmas	member wf, select wf, int seg wf, last wf, assert wf, true wf, not wf, false wf